$\forall$$T$:Type, $x$,$y$:$T$, $L$:($T$ List). \\[0ex]($x$ $\in$ $L$) $\Rightarrow$ ($y$ $\in$ $L$) $\Rightarrow$ ((($x$ = $y$) $\vee$ l\_before($x$; $y$; $L$; $T$)) $\vee$ l\_before($y$; $x$; $L$; $T$))